A:Type, i:, L:A List.
i+1<||L||
 (X, Y:A List.
 (L = (X @ [L[i]; L[i+1]] @ Y) & swap(L;i;i+1) = (X @ [L[i+1]; L[i]] @ Y)  A List) 

latex

Definitions	hd(l), i<j, ij, {T}, SQType(T), P  Q, Dec(P), True, P  Q, T, P  Q, as @ bs, swap(L;i;j), Prop, l[i], i  j < k, {i..j}, ||as||, tl(l), , t  T, x:A. B(x), P  Q, ij, P & Q, x:A. B(x), False, A, AB
Lemmas	ge wf, nat properties, nat wf, length wf1, tl wf, le wf, select wf, swap wf, append wf, squash wf, true wf, length tl, list extensionality, decidable int equal, select cons tl, select tl, swap length, swapped select, list decomp, hd wf, length cons, non neg length, cons one one, member wf, swap cons